Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ModelValueCache rework #2675

Merged
merged 8 commits into from
Aug 10, 2023
Merged

ModelValueCache rework #2675

merged 8 commits into from
Aug 10, 2023

Conversation

Kukovec
Copy link
Collaborator

@Kukovec Kukovec commented Jul 27, 2023

  • Tests added for any new code
  • Ran make fmt-fix (or had formatting run automatically on all files edited)
  • Documentation added for any new functionality
  • Entries added to ./unreleased/ for any new functionality

closes #2664

Note that ModelValueCache is being renamed to UninterpretedLiteralCache, since we're not using the terminology "model value" anymore.

@Kukovec Kukovec requested review from thpani and shonfeder July 27, 2023 15:21
@Kukovec Kukovec requested a review from rodrigo7491 as a code owner July 27, 2023 15:21
Copy link
Contributor

@shonfeder shonfeder left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking good!

I have some questions, mostly for my own edification.

In the future, for there PRs, could you also provide a link to the class you are porting over? I think that is useful context for us reviewers. In this case it is https://github.com/informalsystems/apalache/tree/4e0094ee5d03a068188a85dcdc8ead021b17033e/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala

assert(newArena3 != newArena2 && cell3 != cell2)
}

test("Constraints are only added when addConstraintsForElem is explicitly called, and only once per value") {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

addConstraintsForElem is not used in this test. Should this be

Suggested change
test("Constraints are only added when addConstraintsForElem is explicitly called, and only once per value") {
test("Constraints are only added when addAllConstraints is explicitly called, and only once per value") {

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Incidentally, it doesn't look like addConstaintsForElem is being tested?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good catch, slipped my mind. I am a little torn though, given how impractical calling distinct on single elements is, I should probably try and find a way to discourage/disable invoking the "-ForElem" method.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Funnily enough, adding these tests helped find a logic bug: In ModelValueCache, the line [1]: https://github.com/informalsystems/apalache/blob/4e0094ee5d03a068188a85dcdc8ead021b17033e/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala#L30
In create returns a collection of all other cells of the same type as the newest cell. However, in AbstractCache https://github.com/informalsystems/apalache/blob/4e0094ee5d03a068188a85dcdc8ead021b17033e/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/AbstractCache.scala#L52-L60
performs create before addToCache. If one would have used line [1] as is in addConstaintsForElem, this would create UNSAT constraints, because that method gets called after both create and addToCache, effectively creating distinct(x, ..., x, ...) constraints, since the latest cell is now part of the others collection too.
Note that the addAllConstraints behavior is unaffected by this, so the "normal" use case wouldn't have been affected, but I'm sure we'd be dealing with the single-elem constraints bug down the line.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good find!

@codecov-commenter
Copy link

codecov-commenter commented Jul 28, 2023

Codecov Report

Merging #2675 (7e5f642) into main (b374361) will increase coverage by 0.02%.
The diff coverage is 100.00%.

@@            Coverage Diff             @@
##             main    #2675      +/-   ##
==========================================
+ Coverage   78.47%   78.50%   +0.02%     
==========================================
  Files         458      459       +1     
  Lines       15859    15873      +14     
  Branches     2606     2578      -28     
==========================================
+ Hits        12446    12461      +15     
+ Misses       3413     3412       -1     
Files Changed Coverage Δ
...edRules/aux/caches/UninterpretedLiteralCache.scala 100.00% <100.00%> (ø)

... and 4 files with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

@Kukovec Kukovec requested a review from shonfeder July 28, 2023 12:18
@Kukovec
Copy link
Collaborator Author

Kukovec commented Jul 28, 2023

I'm just going to leave a note here on the difference between batching distincts and adding them incrementally, since GH has nicer formatting than in-code comments.

If we consider a naive implementation of distinct(a1,..., an) as a1 != a2 /\ a1 != a3 /\ ... /\ a{n-1} != an, a distinct with n elements is equivalent to dn = n(n-1)/2 disequalities. Suppose we end up with a collection of N cache values (of a given type). If we called addConstaintsForElem after each addition, we'd end up with d1 + d2 + ... + dN disequalities, i.e.

\sum_{i=1}^N n(n-1)/2 = N(N^2 -1)/6

In contrast, addAllConstraints produces dN = N(N-1)/2 disequalities, which is O(N^2), instead of O(N^3). A pretty good reason to avoid addConstaintsForElem, in favor of addAllConstraints, if possible.

Comment on lines 46 to 51
override def addConstraintsForElem(ctx: SolverContext): (((String, String), ArenaCell)) => Unit = {
case ((tp, _), v) =>
val cellType = if (tp == StrT1.toString) StrT1 else ConstT1(tp)
val others = values().withFilter { c => c.cellType == CellTFrom(cellType) && c != v }.map(_.toBuilder).toSeq
// The fresh cell should differ from the previously created cells.
// We use the SMT constraint (distinct ...).
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why don't we need a check that the entry is actually in the cache?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We could add it, but there's technically nothing wrong is asserting that a value outside the cache is distinct from all values in the cache. Theoretically, once this is wired to some manager class, this method will either:

  • get called once, immediately after an element is added, so membership is established by construction, or
  • never get called in favor of addAll, so the issue is irrelevant

it's just that, at this point in time, I cannot 100% predict what the integration of this class into the rules engine will look like, since it won't exactly be 1-to-1 with ModelValueCache. If you want a QOL exception trigger, I'd be happy to put that in though.

* The UninterpretedLiteralCache maintains that a cell cache for a value `idx` of type `tp` is distinct from all other
* values of type `tp` (defined so far).
*
* Whenever possible, try to use [[addAllConstraints]] instead of this method, for performance reasons instead.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could we just implement this method as a deferred call to addAllConstraints? Is there some reason this one would need to be used instead of addAll?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure exactly what you mean by "deferred", and the overhead of figuring out when to actually resolve it seems to not be worth it to me.
It'd be easier to answer whether or not we need this, when I actually start wiring this up, so that these assertion methods are called by something. At that point, if we see that this one is redundant, we can delete it then.

Copy link
Contributor

@shonfeder shonfeder left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a couple followup questions to be sure I understand the rationale for the choices. Also please do add your comment here on the rationale to the comments in the code. Tat is where will be most useful!! :)

@Kukovec Kukovec requested review from thpani and removed request for thpani August 10, 2023 10:44
@Kukovec
Copy link
Collaborator Author

Kukovec commented Aug 10, 2023

@thpani since Shon is on vacation, could you please finish the review in his stead?

Copy link
Collaborator

@thpani thpani left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, just 2 small questions

))
}

test("Constraints are only added when addAllConstraintsForElem is explicitly called, and only once per value") {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this have a different description? It uses addConstraintsForElem

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, I'll fix the name

Kukovec and others added 2 commits August 10, 2023 13:37
…iedRules/aux/caches/UninterpretedLiteralCache.scala

Co-authored-by: Thomas Pani <[email protected]>
@Kukovec Kukovec enabled auto-merge (squash) August 10, 2023 11:38
@Kukovec Kukovec merged commit d9a9e90 into main Aug 10, 2023
@Kukovec Kukovec deleted the jk/2664 branch August 10, 2023 12:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Rewrite cache: ModelValueCache
4 participants